Matches in value-assignements (V): {{numOfValueMatches}}
Matches in edge-description: {{numOfDescriptionMatches}}
Rank |
Scope |
|||
-V- |
{{line.bestrank}}
|
{{line.desc}}
|
| Precondition (initial variable assignment): |
|
{{precondition}} |
| {{fault.rank}}. | {{fault.score}} | Details: | ||||
Current values:
|
||||||
1 | extern void __VERIFIER_error() __attribute__ ((__noreturn__)); |
2 | |
3 | typedef long unsigned int size_t; |
4 | typedef int wchar_t; |
5 | |
6 | union wait |
7 | { |
8 | int w_status; |
9 | struct |
10 | { |
11 | unsigned int __w_termsig:7; |
12 | unsigned int __w_coredump:1; |
13 | unsigned int __w_retcode:8; |
14 | unsigned int:16; |
15 | } __wait_terminated; |
16 | struct |
17 | { |
18 | unsigned int __w_stopval:8; |
19 | unsigned int __w_stopsig:8; |
20 | unsigned int:16; |
21 | } __wait_stopped; |
22 | }; |
23 | typedef union |
24 | { |
25 | union wait *__uptr; |
26 | int *__iptr; |
27 | } __WAIT_STATUS __attribute__ ((__transparent_union__)); |
28 | |
29 | typedef struct |
30 | { |
31 | int quot; |
32 | int rem; |
33 | } div_t; |
34 | typedef struct |
35 | { |
36 | long int quot; |
37 | long int rem; |
38 | } ldiv_t; |
39 | |
40 | |
41 | __extension__ typedef struct |
42 | { |
43 | long long int quot; |
44 | long long int rem; |
45 | } lldiv_t; |
46 | |
47 | extern size_t __ctype_get_mb_cur_max (void) __attribute__ ((__nothrow__ , __leaf__)) ; |
48 | |
49 | extern double atof (__const char *__nptr) |
50 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ; |
51 | extern int atoi (__const char *__nptr) |
52 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ; |
53 | extern long int atol (__const char *__nptr) |
54 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ; |
55 | |
56 | |
57 | __extension__ extern long long int atoll (__const char *__nptr) |
58 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ; |
59 | |
60 | |
61 | extern double strtod (__const char *__restrict __nptr, |
62 | char **__restrict __endptr) |
63 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
64 | |
65 | |
66 | extern float strtof (__const char *__restrict __nptr, |
67 | char **__restrict __endptr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
68 | extern long double strtold (__const char *__restrict __nptr, |
69 | char **__restrict __endptr) |
70 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
71 | |
72 | |
73 | extern long int strtol (__const char *__restrict __nptr, |
74 | char **__restrict __endptr, int __base) |
75 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
76 | extern unsigned long int strtoul (__const char *__restrict __nptr, |
77 | char **__restrict __endptr, int __base) |
78 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
79 | |
80 | __extension__ |
81 | extern long long int strtoq (__const char *__restrict __nptr, |
82 | char **__restrict __endptr, int __base) |
83 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
84 | __extension__ |
85 | extern unsigned long long int strtouq (__const char *__restrict __nptr, |
86 | char **__restrict __endptr, int __base) |
87 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
88 | |
89 | __extension__ |
90 | extern long long int strtoll (__const char *__restrict __nptr, |
91 | char **__restrict __endptr, int __base) |
92 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
93 | __extension__ |
94 | extern unsigned long long int strtoull (__const char *__restrict __nptr, |
95 | char **__restrict __endptr, int __base) |
96 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
97 | |
98 | extern char *l64a (long int __n) __attribute__ ((__nothrow__ , __leaf__)) ; |
99 | extern long int a64l (__const char *__s) |
100 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ; |
101 | |
102 | typedef unsigned char __u_char; |
103 | typedef unsigned short int __u_short; |
104 | typedef unsigned int __u_int; |
105 | typedef unsigned long int __u_long; |
106 | typedef signed char __int8_t; |
107 | typedef unsigned char __uint8_t; |
108 | typedef signed short int __int16_t; |
109 | typedef unsigned short int __uint16_t; |
110 | typedef signed int __int32_t; |
111 | typedef unsigned int __uint32_t; |
112 | typedef signed long int __int64_t; |
113 | typedef unsigned long int __uint64_t; |
114 | typedef long int __quad_t; |
115 | typedef unsigned long int __u_quad_t; |
116 | typedef unsigned long int __dev_t; |
117 | typedef unsigned int __uid_t; |
118 | typedef unsigned int __gid_t; |
119 | typedef unsigned long int __ino_t; |
120 | typedef unsigned long int __ino64_t; |
121 | typedef unsigned int __mode_t; |
122 | typedef unsigned long int __nlink_t; |
123 | typedef long int __off_t; |
124 | typedef long int __off64_t; |
125 | typedef int __pid_t; |
126 | typedef struct { int __val[2]; } __fsid_t; |
127 | typedef long int __clock_t; |
128 | typedef unsigned long int __rlim_t; |
129 | typedef unsigned long int __rlim64_t; |
130 | typedef unsigned int __id_t; |
131 | typedef long int __time_t; |
132 | typedef unsigned int __useconds_t; |
133 | typedef long int __suseconds_t; |
134 | typedef int __daddr_t; |
135 | typedef long int __swblk_t; |
136 | typedef int __key_t; |
137 | typedef int __clockid_t; |
138 | typedef void * __timer_t; |
139 | typedef long int __blksize_t; |
140 | typedef long int __blkcnt_t; |
141 | typedef long int __blkcnt64_t; |
142 | typedef unsigned long int __fsblkcnt_t; |
143 | typedef unsigned long int __fsblkcnt64_t; |
144 | typedef unsigned long int __fsfilcnt_t; |
145 | typedef unsigned long int __fsfilcnt64_t; |
146 | typedef long int __ssize_t; |
147 | typedef __off64_t __loff_t; |
148 | typedef __quad_t *__qaddr_t; |
149 | typedef char *__caddr_t; |
150 | typedef long int __intptr_t; |
151 | typedef unsigned int __socklen_t; |
152 | typedef __u_char u_char; |
153 | typedef __u_short u_short; |
154 | typedef __u_int u_int; |
155 | typedef __u_long u_long; |
156 | typedef __quad_t quad_t; |
157 | typedef __u_quad_t u_quad_t; |
158 | typedef __fsid_t fsid_t; |
159 | typedef __loff_t loff_t; |
160 | typedef __ino_t ino_t; |
161 | typedef __dev_t dev_t; |
162 | typedef __gid_t gid_t; |
163 | typedef __mode_t mode_t; |
164 | typedef __nlink_t nlink_t; |
165 | typedef __uid_t uid_t; |
166 | typedef __off_t off_t; |
167 | typedef __pid_t pid_t; |
168 | typedef __id_t id_t; |
169 | typedef __ssize_t ssize_t; |
170 | typedef __daddr_t daddr_t; |
171 | typedef __caddr_t caddr_t; |
172 | typedef __key_t key_t; |
173 | |
174 | typedef __clock_t clock_t; |
175 | |
176 | |
177 | |
178 | typedef __time_t time_t; |
179 | |
180 | |
181 | typedef __clockid_t clockid_t; |
182 | typedef __timer_t timer_t; |
183 | typedef unsigned long int ulong; |
184 | typedef unsigned short int ushort; |
185 | typedef unsigned int uint; |
186 | typedef int int8_t __attribute__ ((__mode__ (__QI__))); |
187 | typedef int int16_t __attribute__ ((__mode__ (__HI__))); |
188 | typedef int int32_t __attribute__ ((__mode__ (__SI__))); |
189 | typedef int int64_t __attribute__ ((__mode__ (__DI__))); |
190 | typedef unsigned int u_int8_t __attribute__ ((__mode__ (__QI__))); |
191 | typedef unsigned int u_int16_t __attribute__ ((__mode__ (__HI__))); |
192 | typedef unsigned int u_int32_t __attribute__ ((__mode__ (__SI__))); |
193 | typedef unsigned int u_int64_t __attribute__ ((__mode__ (__DI__))); |
194 | typedef int register_t __attribute__ ((__mode__ (__word__))); |
195 | typedef int __sig_atomic_t; |
196 | typedef struct |
197 | { |
198 | unsigned long int __val[(1024 / (8 * sizeof (unsigned long int)))]; |
199 | } __sigset_t; |
200 | typedef __sigset_t sigset_t; |
201 | struct timespec |
202 | { |
203 | __time_t tv_sec; |
204 | long int tv_nsec; |
205 | }; |
206 | struct timeval |
207 | { |
208 | __time_t tv_sec; |
209 | __suseconds_t tv_usec; |
210 | }; |
211 | typedef __suseconds_t suseconds_t; |
212 | typedef long int __fd_mask; |
213 | typedef struct |
214 | { |
215 | __fd_mask __fds_bits[1024 / (8 * (int) sizeof (__fd_mask))]; |
216 | } fd_set; |
217 | typedef __fd_mask fd_mask; |
218 | |
219 | extern int select (int __nfds, fd_set *__restrict __readfds, |
220 | fd_set *__restrict __writefds, |
221 | fd_set *__restrict __exceptfds, |
222 | struct timeval *__restrict __timeout); |
223 | extern int pselect (int __nfds, fd_set *__restrict __readfds, |
224 | fd_set *__restrict __writefds, |
225 | fd_set *__restrict __exceptfds, |
226 | const struct timespec *__restrict __timeout, |
227 | const __sigset_t *__restrict __sigmask); |
228 | |
229 | |
230 | __extension__ |
231 | extern unsigned int gnu_dev_major (unsigned long long int __dev) |
232 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); |
233 | __extension__ |
234 | extern unsigned int gnu_dev_minor (unsigned long long int __dev) |
235 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); |
236 | __extension__ |
237 | extern unsigned long long int gnu_dev_makedev (unsigned int __major, |
238 | unsigned int __minor) |
239 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); |
240 | |
241 | typedef __blksize_t blksize_t; |
242 | typedef __blkcnt_t blkcnt_t; |
243 | typedef __fsblkcnt_t fsblkcnt_t; |
244 | |
245 | |
246 | typedef __fsfilcnt_t fsfilcnt_t; |
247 | typedef unsigned long int pthread_t; |
248 | typedef union |
249 | { |
250 | char __size[56]; |
251 | long int __align; |
252 | } pthread_attr_t; |
253 | typedef struct __pthread_internal_list |
254 | { |
255 | struct __pthread_internal_list *__prev; |
256 | struct __pthread_internal_list *__next; |
257 | } __pthread_list_t; |
258 | typedef union |
259 | { |
260 | struct __pthread_mutex_s |
261 | { |
262 | int __lock; |
263 | unsigned int __count; |
264 | int __owner; |
265 | unsigned int __nusers; |
266 | int __kind; |
267 | int __spins; |
268 | __pthread_list_t __list; |
269 | } __data; |
270 | char __size[40]; |
271 | long int __align; |
272 | } pthread_mutex_t; |
273 | typedef union |
274 | { |
275 | char __size[4]; |
276 | int __align; |
277 | } pthread_mutexattr_t; |
278 | typedef union |
279 | { |
280 | struct |
281 | { |
282 | int __lock; |
283 | unsigned int __futex; |
284 | __extension__ unsigned long long int __total_seq; |
285 | __extension__ unsigned long long int __wakeup_seq; |
286 | __extension__ unsigned long long int __woken_seq; |
287 | void *__mutex; |
288 | unsigned int __nwaiters; |
289 | unsigned int __broadcast_seq; |
290 | } __data; |
291 | char __size[48]; |
292 | __extension__ long long int __align; |
293 | } pthread_cond_t; |
294 | typedef union |
295 | { |
296 | char __size[4]; |
297 | int __align; |
298 | } pthread_condattr_t; |
299 | typedef unsigned int pthread_key_t; |
300 | typedef int pthread_once_t; |
301 | typedef union |
302 | { |
303 | struct |
304 | { |
305 | int __lock; |
306 | unsigned int __nr_readers; |
307 | unsigned int __readers_wakeup; |
308 | unsigned int __writer_wakeup; |
309 | unsigned int __nr_readers_queued; |
310 | unsigned int __nr_writers_queued; |
311 | int __writer; |
312 | int __shared; |
313 | unsigned long int __pad1; |
314 | unsigned long int __pad2; |
315 | unsigned int __flags; |
316 | } __data; |
317 | char __size[56]; |
318 | long int __align; |
319 | } pthread_rwlock_t; |
320 | typedef union |
321 | { |
322 | char __size[8]; |
323 | long int __align; |
324 | } pthread_rwlockattr_t; |
325 | typedef volatile int pthread_spinlock_t; |
326 | typedef union |
327 | { |
328 | char __size[32]; |
329 | long int __align; |
330 | } pthread_barrier_t; |
331 | typedef union |
332 | { |
333 | char __size[4]; |
334 | int __align; |
335 | } pthread_barrierattr_t; |
336 | |
337 | extern long int random (void) __attribute__ ((__nothrow__ , __leaf__)); |
338 | extern void srandom (unsigned int __seed) __attribute__ ((__nothrow__ , __leaf__)); |
339 | extern char *initstate (unsigned int __seed, char *__statebuf, |
340 | size_t __statelen) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2))); |
341 | |
342 | |
343 | extern char *setstate (char *__statebuf) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
344 | |
345 | |
346 | |
347 | |
348 | |
349 | |
350 | |
351 | struct random_data |
352 | { |
353 | int32_t *fptr; |
354 | int32_t *rptr; |
355 | int32_t *state; |
356 | int rand_type; |
357 | int rand_deg; |
358 | int rand_sep; |
359 | int32_t *end_ptr; |
360 | }; |
361 | |
362 | extern int random_r (struct random_data *__restrict __buf, |
363 | int32_t *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); |
364 | |
365 | extern int srandom_r (unsigned int __seed, struct random_data *__buf) |
366 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2))); |
367 | |
368 | extern int initstate_r (unsigned int __seed, char *__restrict __statebuf, |
369 | size_t __statelen, |
370 | struct random_data *__restrict __buf) |
371 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2, 4))); |
372 | |
373 | extern int setstate_r (char *__restrict __statebuf, |
374 | struct random_data *__restrict __buf) |
375 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); |
376 | |
377 | |
378 | |
379 | |
380 | |
381 | |
382 | extern int rand (void) __attribute__ ((__nothrow__ , __leaf__)); |
383 | |
384 | extern void srand (unsigned int __seed) __attribute__ ((__nothrow__ , __leaf__)); |
385 | |
386 | |
387 | |
388 | |
389 | extern int rand_r (unsigned int *__seed) __attribute__ ((__nothrow__ , __leaf__)); |
390 | |
391 | |
392 | |
393 | |
394 | |
395 | |
396 | |
397 | extern double drand48 (void) __attribute__ ((__nothrow__ , __leaf__)); |
398 | extern double erand48 (unsigned short int __xsubi[3]) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
399 | |
400 | |
401 | extern long int lrand48 (void) __attribute__ ((__nothrow__ , __leaf__)); |
402 | extern long int nrand48 (unsigned short int __xsubi[3]) |
403 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
404 | |
405 | |
406 | extern long int mrand48 (void) __attribute__ ((__nothrow__ , __leaf__)); |
407 | extern long int jrand48 (unsigned short int __xsubi[3]) |
408 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
409 | |
410 | |
411 | extern void srand48 (long int __seedval) __attribute__ ((__nothrow__ , __leaf__)); |
412 | extern unsigned short int *seed48 (unsigned short int __seed16v[3]) |
413 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
414 | extern void lcong48 (unsigned short int __param[7]) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
415 | |
416 | |
417 | |
418 | |
419 | |
420 | struct drand48_data |
421 | { |
422 | unsigned short int __x[3]; |
423 | unsigned short int __old_x[3]; |
424 | unsigned short int __c; |
425 | unsigned short int __init; |
426 | unsigned long long int __a; |
427 | }; |
428 | |
429 | |
430 | extern int drand48_r (struct drand48_data *__restrict __buffer, |
431 | double *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); |
432 | extern int erand48_r (unsigned short int __xsubi[3], |
433 | struct drand48_data *__restrict __buffer, |
434 | double *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); |
435 | |
436 | |
437 | extern int lrand48_r (struct drand48_data *__restrict __buffer, |
438 | long int *__restrict __result) |
439 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); |
440 | extern int nrand48_r (unsigned short int __xsubi[3], |
441 | struct drand48_data *__restrict __buffer, |
442 | long int *__restrict __result) |
443 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); |
444 | |
445 | |
446 | extern int mrand48_r (struct drand48_data *__restrict __buffer, |
447 | long int *__restrict __result) |
448 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); |
449 | extern int jrand48_r (unsigned short int __xsubi[3], |
450 | struct drand48_data *__restrict __buffer, |
451 | long int *__restrict __result) |
452 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); |
453 | |
454 | |
455 | extern int srand48_r (long int __seedval, struct drand48_data *__buffer) |
456 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2))); |
457 | |
458 | extern int seed48_r (unsigned short int __seed16v[3], |
459 | struct drand48_data *__buffer) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); |
460 | |
461 | extern int lcong48_r (unsigned short int __param[7], |
462 | struct drand48_data *__buffer) |
463 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); |
464 | |
465 | |
466 | |
467 | |
468 | |
469 | |
470 | |
471 | |
472 | |
473 | extern void *malloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ; |
474 | |
475 | extern void *calloc (size_t __nmemb, size_t __size) |
476 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ; |
477 | |
478 | |
479 | |
480 | |
481 | |
482 | |
483 | |
484 | |
485 | |
486 | |
487 | extern void *realloc (void *__ptr, size_t __size) |
488 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__warn_unused_result__)); |
489 | |
490 | extern void free (void *__ptr) __attribute__ ((__nothrow__ , __leaf__)); |
491 | |
492 | |
493 | |
494 | |
495 | extern void cfree (void *__ptr) __attribute__ ((__nothrow__ , __leaf__)); |
496 | |
497 | extern void *alloca (size_t __size) __attribute__ ((__nothrow__ , __leaf__)); |
498 | |
499 | |
500 | |
501 | |
502 | |
503 | |
504 | |
505 | extern void *valloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ; |
506 | |
507 | |
508 | |
509 | |
510 | extern int posix_memalign (void **__memptr, size_t __alignment, size_t __size) |
511 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
512 | |
513 | |
514 | |
515 | |
516 | extern void abort (void) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); |
517 | |
518 | |
519 | |
520 | extern int atexit (void (*__func) (void)) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
521 | |
522 | extern int on_exit (void (*__func) (int __status, void *__arg), void *__arg) |
523 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
524 | |
525 | extern void exit (int __status) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); |
526 | |
527 | |
528 | extern void _Exit (int __status) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); |
529 | |
530 | |
531 | extern char *getenv (__const char *__name) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
532 | |
533 | extern char *__secure_getenv (__const char *__name) |
534 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
535 | extern int putenv (char *__string) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
536 | extern int setenv (__const char *__name, __const char *__value, int __replace) |
537 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2))); |
538 | extern int unsetenv (__const char *__name) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
539 | extern int clearenv (void) __attribute__ ((__nothrow__ , __leaf__)); |
540 | extern char *mktemp (char *__template) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
541 | extern int mkstemp (char *__template) __attribute__ ((__nonnull__ (1))) ; |
542 | extern int mkstemps (char *__template, int __suffixlen) __attribute__ ((__nonnull__ (1))) ; |
543 | extern char *mkdtemp (char *__template) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
544 | |
545 | extern int system (__const char *__command) ; |
546 | |
547 | extern char *realpath (__const char *__restrict __name, |
548 | char *__restrict __resolved) __attribute__ ((__nothrow__ , __leaf__)) ; |
549 | typedef int (*__compar_fn_t) (__const void *, __const void *); |
550 | |
551 | extern void *bsearch (__const void *__key, __const void *__base, |
552 | size_t __nmemb, size_t __size, __compar_fn_t __compar) |
553 | __attribute__ ((__nonnull__ (1, 2, 5))) ; |
554 | extern void qsort (void *__base, size_t __nmemb, size_t __size, |
555 | __compar_fn_t __compar) __attribute__ ((__nonnull__ (1, 4))); |
556 | extern int abs (int __x) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ; |
557 | extern long int labs (long int __x) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ; |
558 | |
559 | __extension__ extern long long int llabs (long long int __x) |
560 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ; |
561 | |
562 | extern div_t div (int __numer, int __denom) |
563 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ; |
564 | extern ldiv_t ldiv (long int __numer, long int __denom) |
565 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ; |
566 | |
567 | |
568 | __extension__ extern lldiv_t lldiv (long long int __numer, |
569 | long long int __denom) |
570 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ; |
571 | |
572 | extern char *ecvt (double __value, int __ndigit, int *__restrict __decpt, |
573 | int *__restrict __sign) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ; |
574 | extern char *fcvt (double __value, int __ndigit, int *__restrict __decpt, |
575 | int *__restrict __sign) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ; |
576 | extern char *gcvt (double __value, int __ndigit, char *__buf) |
577 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))) ; |
578 | extern char *qecvt (long double __value, int __ndigit, |
579 | int *__restrict __decpt, int *__restrict __sign) |
580 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ; |
581 | extern char *qfcvt (long double __value, int __ndigit, |
582 | int *__restrict __decpt, int *__restrict __sign) |
583 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ; |
584 | extern char *qgcvt (long double __value, int __ndigit, char *__buf) |
585 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))) ; |
586 | extern int ecvt_r (double __value, int __ndigit, int *__restrict __decpt, |
587 | int *__restrict __sign, char *__restrict __buf, |
588 | size_t __len) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5))); |
589 | extern int fcvt_r (double __value, int __ndigit, int *__restrict __decpt, |
590 | int *__restrict __sign, char *__restrict __buf, |
591 | size_t __len) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5))); |
592 | extern int qecvt_r (long double __value, int __ndigit, |
593 | int *__restrict __decpt, int *__restrict __sign, |
594 | char *__restrict __buf, size_t __len) |
595 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5))); |
596 | extern int qfcvt_r (long double __value, int __ndigit, |
597 | int *__restrict __decpt, int *__restrict __sign, |
598 | char *__restrict __buf, size_t __len) |
599 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5))); |
600 | |
601 | extern int mblen (__const char *__s, size_t __n) __attribute__ ((__nothrow__ , __leaf__)) ; |
602 | extern int mbtowc (wchar_t *__restrict __pwc, |
603 | __const char *__restrict __s, size_t __n) __attribute__ ((__nothrow__ , __leaf__)) ; |
604 | extern int wctomb (char *__s, wchar_t __wchar) __attribute__ ((__nothrow__ , __leaf__)) ; |
605 | extern size_t mbstowcs (wchar_t *__restrict __pwcs, |
606 | __const char *__restrict __s, size_t __n) __attribute__ ((__nothrow__ , __leaf__)); |
607 | extern size_t wcstombs (char *__restrict __s, |
608 | __const wchar_t *__restrict __pwcs, size_t __n) |
609 | __attribute__ ((__nothrow__ , __leaf__)); |
610 | |
611 | extern int rpmatch (__const char *__response) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
612 | extern int getsubopt (char **__restrict __optionp, |
613 | char *__const *__restrict __tokens, |
614 | char **__restrict __valuep) |
615 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2, 3))) ; |
616 | extern int getloadavg (double __loadavg[], int __nelem) |
617 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
618 | |
619 | extern int __VERIFIER_nondet_int(void); |
620 | struct node { |
621 | int value; |
622 | struct node *next; |
623 | }; |
624 | struct list { |
625 | struct node *slist; |
626 | struct list *next; |
627 | }; |
628 | struct iterator { |
629 | struct list *list; |
630 | struct node *node; |
631 | }; |
632 | int main() |
633 | { |
634 | struct list *data = ((void *)0); |
635 | { |
636 | while (__VERIFIER_nondet_int()) |
637 | { |
638 | struct node *node = malloc(sizeof *node); |
639 | if (!node) |
640 | abort(); |
641 | node->next = ((void *)0); |
642 | node->value = __VERIFIER_nondet_int(); |
643 | struct list *item = malloc(sizeof *item); |
644 | if (!item) |
645 | abort(); |
646 | item->slist = node; |
647 | item->next = data; |
648 | data = item; |
649 | } |
650 | } |
651 | { |
652 | struct iterator iter; |
653 | { |
654 | struct list *list = data; |
655 | if ((iter.list = list)) |
656 | iter.node = list->slist; |
657 | } |
658 | struct node *node; |
659 | { |
660 | if (!iter.list) |
661 | node = ((void *)0); |
662 | else { |
663 | struct node *current = iter.node; |
664 | if ((iter.node = current->next)) |
665 | node = current; |
666 | else { |
667 | if ((iter.list = iter.list->next)) |
668 | iter.node = iter.list->slist; |
669 | node = current; |
670 | } |
671 | } |
672 | } |
673 | while ((node)) |
674 | { |
675 | { |
676 | if (!iter.list) |
677 | node = ((void *)0); |
678 | else { |
679 | struct node *current = iter.node; |
680 | if ((iter.node = current->next)) |
681 | node = current; |
682 | else { |
683 | if ((iter.list = iter.list->next)) |
684 | iter.node = iter.list->slist; |
685 | node = current; |
686 | } |
687 | } |
688 | } |
689 | } |
690 | } |
691 | { |
692 | struct list *list = data; |
693 | while (list && list->next) { |
694 | struct list *dst = ((void *)0); |
695 | while (list) { |
696 | struct list *next = list->next; |
697 | if (!next) { |
698 | list->next = dst; |
699 | dst = list; |
700 | break; |
701 | } |
702 | { struct node **dst = &list->slist; |
703 | struct node *sub1 = list->slist; |
704 | struct node *sub2 = next->slist; |
705 | while (sub1 || sub2) { |
706 | struct node ***pdst = &dst; |
707 | struct node **pdata; |
708 | if (!sub2 || (sub1 && __VERIFIER_nondet_int())) |
709 | pdata = &sub1; |
710 | else |
711 | pdata = &sub2; |
712 | struct node *node = *pdata; |
713 | *pdata = node->next; |
714 | node->next = ((void *)0); |
715 | **pdst = node; |
716 | *pdst = &node->next; |
717 | } |
718 | } |
719 | list->next = dst; |
720 | dst = list; |
721 | list = next->next; |
722 | free(next); |
723 | } |
724 | list = dst; |
725 | } |
726 | data = list; |
727 | } |
728 | { |
729 | struct iterator iter; |
730 | { |
731 | struct list *list = data; |
732 | if ((iter.list = list)) |
733 | iter.node = list->slist; |
734 | } |
735 | struct node *node; |
736 | { |
737 | if (!iter.list) |
738 | node = ((void *)0); |
739 | else { |
740 | struct node *current = iter.node; |
741 | if ((iter.node = current->next)) |
742 | node = current; |
743 | else { |
744 | if ((iter.list = iter.list->next)) |
745 | iter.node = iter.list->slist; |
746 | node = current; |
747 | } |
748 | } |
749 | } |
750 | while ((node)) |
751 | { |
752 | { |
753 | if (!iter.list) |
754 | node = ((void *)0); |
755 | else { |
756 | struct node *current = iter.node; |
757 | if ((iter.node = current->next)) |
758 | node = current; |
759 | else { |
760 | if ((iter.list = iter.list->next)) |
761 | iter.node = iter.list->slist; |
762 | node = current; |
763 | } |
764 | } |
765 | } |
766 | } |
767 | } |
768 | { |
769 | while (data) { |
770 | struct list *next = data->next; |
771 | struct node *node = data->slist; |
772 | while (node) { |
773 | struct node *snext = node->next; |
774 | free(node); |
775 | node = snext; |
776 | } |
777 | free(data); |
778 | data = next; |
779 | } |
780 | } |
781 | return 0; |
782 | } |
| Date | Time | Level | Component | Message |
|---|---|---|---|---|
| 2025-08-28 | 16:16:33:182 | INFO | CPAMain.detectFrontendLanguageIfNecessary | Language C detected and set for analysis |
| 2025-08-28 | 16:16:33:263 | INFO | CPAchecker.run | CPAchecker 4.0 / terminationAnalysis (OpenJDK 64-Bit Server VM 17.0.15) started |
| 2025-08-28 | 16:16:33:282 | INFO | CPAchecker.parse | Parsing CFA from file(s) "Benchmarks/TermCOMP/C/SV-COMP_Mixed_Categories/test-0521_true-valid-memsafety/test-0521_true-valid-memsafety.c" |
| 2025-08-28 | 16:16:34:656 | INFO | CoreComponentsFactory.createAlgorithm | Using Restarting Algorithm |
| 2025-08-28 | 16:16:34:677 | WARNING | CPAchecker.printConfigurationWarnings | The following configuration options were specified but are not used: cpa.arg.lateMerge counterexample.export.exportWitness |
| 2025-08-28 | 16:16:34:677 | INFO | CPAchecker.runAlgorithm | Starting analysis ... |
| 2025-08-28 | 16:16:34:687 | INFO | RestartAlgorithm.run | Loading analysis 1 from file /cpachecker/config/components/combinations-parallel-termination.properties ... |
| 2025-08-28 | 16:16:34:726 | INFO | Analysis /cpachecker/config/components/combinations-parallel-termination.properties Parallel analysis 1 ResourceLimitChecker.fromConfiguration | Using the following resource limits: Thread CPU-time limit of 300s |
| 2025-08-28 | 16:16:35:074 | INFO | Analysis /cpachecker/config/components/combinations-parallel-termination.properties Parallel analysis 1 PredicateCPA PredicateCPA.<init> | Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21. |
| 2025-08-28 | 16:16:35:460 | INFO | Analysis /cpachecker/config/components/combinations-parallel-termination.properties Parallel analysis 1 PredicateCPA PredicateCPARefiner.<init> | Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. |
| 2025-08-28 | 16:16:35:473 | WARNING | CPAs.retrieveCPAOrFail | Warning: Skipping one analysis because the configuration file /cpachecker/config/components/combinations-parallel-termination.properties is invalid (TerminationAlgorithm needs a TerminationCPA) |
| 2025-08-28 | 16:16:35:476 | INFO | RestartAlgorithm.run | Loading analysis 1 from file /cpachecker/config/components/termination-recursion.properties ... |
| 2025-08-28 | 16:16:35:484 | INFO | NestingAlgorithm.checkConfigs | Mismatch of configuration options when loading from '/cpachecker/config/components/termination-recursion.properties': 'termination.config' has two values 'terminationAnalysis.properties' and 'termination-recursion.properties'. Using 'termination-recursion.properties'. |
| 2025-08-28 | 16:16:35:507 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties PredicateCPA FormulaManagerView.<init> | Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics. |
| 2025-08-28 | 16:16:35:510 | INFO | Analysis /cpachecker/config/components/termination-recursion.properties PredicateCPA PredicateCPA.<init> | Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21. |
| 2025-08-28 | 16:16:35:717 | INFO | Analysis /cpachecker/config/components/termination-recursion.properties PredicateCPA PredicateCPARefiner.<init> | Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. |
| 2025-08-28 | 16:16:35:785 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties FormulaManagerView.<init> | Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics. |
| 2025-08-28 | 16:16:35:820 | INFO | RestartAlgorithm.run | Starting analysis 1 ... |
| 2025-08-28 | 16:16:35:821 | INFO | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.run0 | Starting termination algorithm. |
| 2025-08-28 | 16:16:43:252 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties InequalityConverter.convert | Warning: Could not extract lasso (Loop with heads [N153] incoming: [line 772: N152 -{while}-> N153] outgoing: [line 772: N153 -{[node__4 == 0]}-> N155] nodes: [N153, N154, N156, N157, N158] ). (Unknown sort in equality) |
| 2025-08-28 | 16:16:43:255 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-28 | 16:16:45:778 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties InequalityConverter.convert | Warning: Could not extract lasso (Loop with heads [N153] incoming: [line 772: N152 -{while}-> N153] outgoing: [line 772: N153 -{[node__4 == 0]}-> N155] nodes: [N153, N154, N156, N157, N158] ). (Unknown sort in equality) |
| 2025-08-28 | 16:16:45:782 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-28 | 16:16:48:079 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties InequalityConverter.convert | Warning: Could not extract lasso (Loop with heads [N153] incoming: [line 772: N152 -{while}-> N153] outgoing: [line 772: N153 -{[node__4 == 0]}-> N155] nodes: [N153, N154, N156, N157, N158] ). (Unknown sort in equality) |
| 2025-08-28 | 16:16:48:080 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-28 | 16:16:50:244 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties InequalityConverter.convert | Warning: Could not extract lasso (Loop with heads [N153] incoming: [line 772: N152 -{while}-> N153] outgoing: [line 772: N153 -{[node__4 == 0]}-> N155] nodes: [N153, N154, N156, N157, N158] ). (Unknown sort in equality) |
| 2025-08-28 | 16:16:50:245 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-28 | 16:16:52:319 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties InequalityConverter.convert | Warning: Could not extract lasso (Loop with heads [N153] incoming: [line 772: N152 -{while}-> N153] outgoing: [line 772: N153 -{[node__4 == 0]}-> N155] nodes: [N153, N154, N156, N157, N158] ). (Unknown sort in equality) |
| 2025-08-28 | 16:16:52:320 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-28 | 16:16:52:644 | SEVERE | RefinementFailedException.forInterpolationFailureInSolver | Error: Refinement failed: Interpolation failed in solver MATHSAT5 with message 'uncolorable Array proof'. |
| Statistics Name | Statistics Value | Additional Value |
|---|---|---|
| Restart Algorithm statistics | ||
| Number of algorithms provided | 2 | |
| Number of algorithms used | 1 | |
| Last algorithm used | /cpachecker/config/components/combinations-parallel-termination.properties | |
| Total time for algorithm 1 | 17.957s | |
| PredicateCPA statistics | ||
| Number of abstractions | 380 | 3% of all post computations |
| Times abstraction was reused | 0 | |
| Because of function entry/exit | 0 | 0% |
| Because of loop head | 366 | 96% |
| Because of join nodes | 0 | 0% |
| Because of threshold | 0 | 0% |
| Because of target state | 14 | 4% |
| Times precision was empty | 73 | 19% |
| Times precision was {false} | 10 | 3% |
| Times result was cached | 107 | 28% |
| Times cartesian abs was used | 0 | 0% |
| Times boolean abs was used | 190 | 50% |
| Times result was 'false' | 41 | 11% |
| Number of strengthen sat checks | 0 | |
| Number of coverage checks | 8120 | |
| BDD entailment checks | 737 | |
| Number of SMT sat checks | 0 | |
| trivial | 0 | |
| cached | 0 | |
| Max ABE block size | 62 | |
| Avg ABE block size | 15.38 | sum: 5846, count: 380, min: 0, max: 62 |
| Number of predicates discovered | 23 | |
| Number of abstraction locations | 8 | |
| Max number of predicates per location | 9 | |
| Avg number of predicates per location | 6 | |
| Total predicates per abstraction | 1483 | |
| Max number of predicates per abstraction | 9 | |
| Avg number of predicates per abstraction | 7.42 | |
| Number of irrelevant predicates | 236 | 16% |
| Number of preds handled by boolean abs | 784 | 53% |
| Total number of models for allsat | 566 | |
| Max number of models for allsat | 24 | |
| Avg number of models for allsat | 2.98 | |
| Time for post operator | 1.332s | |
| Time for path formula creation | 1.314s | |
| Time for strengthen operator | 0.035s | |
| Time for prec operator | 0.858s | |
| Time for abstraction | 0.794s | Max: 0.016s, Count: 380 |
| Boolean abstraction | 0.405s | |
| Solving time | 0.221s | Max: 0.007s |
| Model enumeration time | 0.153s | |
| Time for BDD construction | 0.048s | Max: 0.002s |
| Time for merge operator | 0.048s | |
| Time for coverage checks | 0.012s | |
| Time for BDD entailment checks | 0.011s | |
| Total time for SMT solver (w/o itp) | 0.374s | |
| Number of path formula cache hits | 7183 | 50% |
| Inside post operator | ||
| Inside path formula creation | ||
| Time for path formula computation | 1.269s | |
| Total number of created targets for pointer analysis | 0 | |
| Number of BDD nodes | 1584 | |
| Size of BDD node table | 466043 | |
| Size of BDD cache | 46619 | |
| Size of BDD node cleanup queue | 0.44 | sum: 1121, count: 2540, min: 0, max: 356 |
| Time for BDD node cleanup | 0.004s | |
| Time for BDD garbage collection | 0.000s | in 0 runs |
| KeyValue statistics | ||
| Init. function predicates | 0 | |
| Init. global predicates | 0 | |
| Init. location predicates | 0 | |
| Invariant Generation statistics | ||
| AutomatonAnalysis (NonTerminationLabelAutomaton) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.052s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 11974, count: 11974, min: 1, max: 1 [1 x 11974] |
| Number of states with assumption transitions | 0 | |
| AutomatonAnalysis (TerminatingFunctions) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.016s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 11938, count: 11974, min: 0, max: 1 [0 x 36, 1 x 11938] |
| Number of states with assumption transitions | 0 | |
| Termination Algorithm statistics | ||
| Total time | 16.822s | |
| Time for recursion analysis | 0.000s | |
| Number of analysed loops | 1 | 13% |
| Total time for loop analysis | 16.817s | |
| Avg time per loop analysis | 16.817s | |
| Max time per loop analysis | 16.817s | |
| Number of safety analysis runs | 6 | |
| Avg safety analysis run per loop | 6.00 | |
| Max safety analysis run per loop | 6 for loops [N153] | |
| Total time for safety analysis | 4.667s | |
| Avg time per safety analysis run | 0.777s | |
| Max time per safety analysis run | 2.238s | |
| Number of analysed lassos | 0 | |
| Avg number of lassos per loop | 0.00 | |
| Max number of lassos per loop | 0 for loops | |
| Avg number of lassos per iteration | 0.00 | |
| Max number of lassos per iteration | 0 | |
| Total time for lassos analysis | 12.126s | |
| Avg time per iteration | 2.425s | |
| Max time per iteration | 5.183s | |
| Time for lassos construction | 12.126s | |
| Avg time for lasso construction per iteration | 2.425s | |
| Max time for lasso construction per iteration | 5.183s | |
| Time for stem and loop construction | 0.314s | |
| Avg time for stem and loop construction per iteration | 0.062s | |
| Max time for stem and loop construction per iteration | 0.214s | |
| Time for lassos creation | 11.792s | |
| Avg time for lassos creation per iteration | 2.358s | |
| Max time for lassos creation per iteration | 4.961s | |
| Total time for non-termination analysis | 0.000s | |
| Avg time for non-termination analysis per lasso | 0.000s | |
| Max time for non-termination analysis per lasso | 0.000s | |
| Total time for termination analysis | 0.000s | |
| Avg time for termination analysis per lasso | 0.000s | |
| Max time for termination analysis per lasso | 0.000s | |
| Total number of termination arguments | 0 | |
| Avg termination arguments per loop | 0.00 | |
| Max termination arguments per loop | 0 for loops | |
| Counterexample-Check Algorithm statistics | ||
| Number of counterexample checks | 0 | |
| Termination Algorithm statistics | ||
| Total time | 16.822s | |
| Time for recursion analysis | 0.000s | |
| Number of analysed loops | 1 | 13% |
| Total time for loop analysis | 16.817s | |
| Avg time per loop analysis | 16.817s | |
| Max time per loop analysis | 16.817s | |
| Number of safety analysis runs | 6 | |
| Avg safety analysis run per loop | 6.00 | |
| Max safety analysis run per loop | 6 for loops [N153] | |
| Total time for safety analysis | 4.667s | |
| Avg time per safety analysis run | 0.777s | |
| Max time per safety analysis run | 2.238s | |
| Number of analysed lassos | 0 | |
| Avg number of lassos per loop | 0.00 | |
| Max number of lassos per loop | 0 for loops | |
| Avg number of lassos per iteration | 0.00 | |
| Max number of lassos per iteration | 0 | |
| Total time for lassos analysis | 12.126s | |
| Avg time per iteration | 2.425s | |
| Max time per iteration | 5.183s | |
| Time for lassos construction | 12.126s | |
| Avg time for lasso construction per iteration | 2.425s | |
| Max time for lasso construction per iteration | 5.183s | |
| Time for stem and loop construction | 0.314s | |
| Avg time for stem and loop construction per iteration | 0.062s | |
| Max time for stem and loop construction per iteration | 0.214s | |
| Time for lassos creation | 11.792s | |
| Avg time for lassos creation per iteration | 2.358s | |
| Max time for lassos creation per iteration | 4.961s | |
| Total time for non-termination analysis | 0.000s | |
| Avg time for non-termination analysis per lasso | 0.000s | |
| Max time for non-termination analysis per lasso | 0.000s | |
| Total time for termination analysis | 0.000s | |
| Avg time for termination analysis per lasso | 0.000s | |
| Max time for termination analysis per lasso | 0.000s | |
| Total number of termination arguments | 0 | |
| Avg termination arguments per loop | 0.00 | |
| Max termination arguments per loop | 0 for loops | |
| Counterexample-Check Algorithm statistics | ||
| Number of counterexample checks | 0 | |
| Code Coverage | ||
| Function coverage | 1.000 | |
| Visited lines | 377 | |
| Total lines | 380 | |
| Line coverage | 0.992 | |
| Visited conditions | 60 | |
| Total conditions | 60 | |
| Condition coverage | 1.000 | |
| CPAchecker general statistics | ||
| Number of program locations | 412 | |
| Number of CFA edges (per node) | 437 | count: 412, min: 0, max: 2, avg: 1.06 |
| Number of relevant variables | 27 | |
| Number of functions | 1 | |
| Number of loops (and loop nodes) | 8 | sum: 158, min: 5, max: 40, avg: 19.75 |
| Size of reached set | 543 | |
| Number of reached locations | 121 | 29% |
| Avg states per location | 4 | |
| Max states per location | 12 | at node N154 |
| Number of reached functions | 1 | 100% |
| Number of partitions | 121 | |
| Avg size of partitions | 4 | |
| Max size of partitions | 12 | with key N154 |
| Number of target states | 1 | |
| Size of final wait list | 17 | |
| Time for analysis setup | 1.396s | |
| Time for loading CPAs | 0.020s | |
| Time for loading parser | 0.211s | |
| Time for CFA construction | 1.123s | |
| Time for parsing file(s) | 0.394s | |
| Time for AST to CFA | 0.319s | |
| Time for CFA sanity check | 0.057s | |
| Time for post-processing | 0.208s | |
| Time for loop structure | 0.019s | |
| Time for AST structure | 0.000s | |
| Time for CFA export | 0.548s | |
| Time for function pointers resolving | 0.005s | |
| Function calls via function pointers | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer calls | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Function calls with function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Time for classifying variables | 0.109s | |
| Time for collecting variables | 0.070s | |
| Time for solving dependencies | 0.004s | |
| Time for building hierarchy | 0.000s | |
| Time for building classification | 0.030s | |
| Time for exporting data | 0.005s | |
| Time for Analysis | 17.959s | |
| CPU time for analysis | 37.040s | |
| Total time for CPAchecker | 19.366s | |
| Total CPU time for CPAchecker | 39.470s | |
| Time for statistics | 0.198s | |
| Time for Garbage Collector | 0.222s | in 122 runs |
| Garbage Collector(s) used | PS MarkSweep, PS Scavenge | |
| Used heap memory | 126MB ( 120 MiB) max; 66MB ( 63 MiB) avg; 140MB ( 133 MiB) peak | |
| Used non-heap memory | 65MB ( 62 MiB) max; 56MB ( 54 MiB) avg; 67MB ( 64 MiB) peak | |
| Used in PS Old Gen pool | 44MB ( 42 MiB) max; 31MB ( 29 MiB) avg; 44MB ( 42 MiB) peak | |
| Allocated heap memory | 261MB ( 249 MiB) max; 254MB ( 242 MiB) avg | |
| Allocated non-heap memory | 68MB ( 65 MiB) max; 60MB ( 57 MiB) avg | |
| Total process virtual memory | 14914MB ( 14223 MiB) max; 14868MB ( 14179 MiB) avg |
| # | Configuration Name | Configuration Value |
|---|---|---|
| 1 | analysis.algorithm.termination | true |
| 2 | analysis.machineModel | Linux64 |
| 3 | analysis.name | terminationAnalysis |
| 4 | analysis.programNames | Benchmarks/TermCOMP/C/SV-COMP_Mixed_Categories/test-0521_true-valid-memsafety/test-0521_true-valid-memsafety.c |
| 5 | analysis.restartAfterUnknown | true |
| 6 | counterexample.export.exportWitness | false |
| 7 | cpa.arg.lateMerge | prevent |
| 8 | language | C |
| 9 | log.level | INFO |
| 10 | parser.usePreprocessor | true |
| 11 | restartAlgorithm.configFiles | components/combinations-parallel-termination.properties, components/termination-recursion.properties::if-recursive |
| 12 | specification | |
| 13 | statistics.print | true |
| 14 | termination.config | terminationAnalysis.properties |
This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.
License: Apache 2.0 License
Source: {{dependency.repository}}
{{dependency.copyright}}
License:
Full text of license
{{dependencies.licenses[dependency.licenseId]}}